{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "import json\n",
    "from bqm_input_checker import InputChecker\n",
    "from btor2bqm import BTor2BQM"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The code we execute: \n",
    "\n",
    "```C\n",
    "uint64_t* x;\n",
    "uint64_t main() { \n",
    "    uint64_t a;\n",
    "    x = malloc(1); // rounded up to 8\n",
    "    \n",
    "    // touch to trigger page fault here\n",
    "    *x = 0;\n",
    "    // read 1 byte from console into x\n",
    "    read(0, x, 1);\n",
    "    a = *x;\n",
    "    a = *(x + a); // segfault if input != 0\n",
    "}\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 32 bit example (u3.btor2)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "```` bash\n",
    "./modeler-32 -c u3.c - 0 --no-syscall-id-check --no-exit-code-check --no-division-by-zero-check --no-address-alignment-check --constant-propagation --linear-address-space\n",
    "````"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "started building ../btor2files/u3.btor2 for 15 timesteps\n",
      "{'size_datasegment': 2, 'size_heap': 1, 'size_stack': 10, 'begin_datasegment': 17408, 'begin_heap': 18432, 'word_size': 32, 'address_step_size': 1, 'address_word_size': 30, 'begin_stack': 1073741824}\n",
      "output dir:  ../all_bad_small_sample/\n",
      "sort memory modified to be bitvector of size:  416\n"
     ]
    }
   ],
   "source": [
    "parser = BTor2BQM(15)\n",
    "bqm = parser.parse_file(f\"../dummy_btor2files/u3.btor2\",\n",
    "                  f\"../all_bad_small_sample/\",\n",
    "                  with_init=True, modify_memory_sort=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "351"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "len(bqm.linear.keys())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0:  2.0 []\n",
      "1:  0.0 [80000009]\n",
      "2:  0.0 [80000009]\n",
      "3:  0.0 [80000009]\n",
      "4:  0.0 [80000009]\n",
      "5:  0.0 [80000009]\n",
      "6:  0.0 [80000009]\n",
      "7:  0.0 [80000009]\n",
      "8:  0.0 [80000009]\n",
      "9:  0.0 [80000009]\n",
      "10:  0.0 [80000009]\n",
      "11:  0.0 [80000009]\n",
      "12:  0.0 [80000009]\n",
      "13:  0.0 [80000009]\n",
      "14:  0.0 [80000009]\n",
      "15:  0.0 [80000009]\n",
      "16:  0.0 [80000009]\n",
      "17:  0.0 [80000009]\n",
      "18:  0.0 [80000009]\n",
      "19:  0.0 [80000009]\n",
      "20:  0.0 [80000009]\n",
      "21:  0.0 [80000009]\n",
      "22:  0.0 [80000009]\n",
      "23:  0.0 [80000009]\n",
      "24:  0.0 [80000009]\n",
      "25:  0.0 [80000009]\n",
      "26:  0.0 [80000009]\n",
      "27:  0.0 [80000009]\n",
      "28:  0.0 [80000009]\n",
      "29:  0.0 [80000009]\n",
      "30:  0.0 [80000009]\n",
      "31:  0.0 [80000009]\n",
      "32:  0.0 [80000009]\n",
      "33:  0.0 [80000009]\n",
      "34:  0.0 [80000009]\n",
      "35:  0.0 [80000009]\n",
      "36:  0.0 [80000009]\n",
      "37:  0.0 [80000009]\n",
      "38:  0.0 [80000009]\n",
      "39:  0.0 [80000009]\n",
      "40:  0.0 [80000009]\n",
      "41:  0.0 [80000009]\n",
      "42:  0.0 [80000009]\n",
      "43:  0.0 [80000009]\n",
      "44:  0.0 [80000009]\n",
      "45:  0.0 [80000009]\n",
      "46:  0.0 [80000009]\n",
      "47:  0.0 [80000009]\n",
      "48:  0.0 [80000009]\n",
      "49:  0.0 [80000009]\n",
      "50:  0.0 [80000009]\n",
      "51:  0.0 [80000009]\n",
      "52:  0.0 [80000009]\n",
      "53:  0.0 [80000009]\n",
      "54:  0.0 [80000009]\n",
      "55:  0.0 [80000009]\n",
      "56:  0.0 [80000009]\n",
      "57:  0.0 [80000009]\n",
      "58:  0.0 [80000009]\n",
      "59:  0.0 [80000009]\n",
      "60:  0.0 [80000009]\n",
      "61:  0.0 [80000009]\n",
      "62:  0.0 [80000009]\n",
      "63:  0.0 [80000009]\n",
      "64:  0.0 [80000009]\n",
      "65:  0.0 [80000009]\n",
      "66:  0.0 [80000009]\n",
      "67:  0.0 [80000009]\n",
      "68:  0.0 [80000009]\n",
      "69:  0.0 [80000009]\n",
      "70:  0.0 [80000009]\n",
      "71:  0.0 [80000009]\n",
      "72:  0.0 [80000009]\n",
      "73:  0.0 [80000009]\n",
      "74:  0.0 [80000009]\n",
      "75:  0.0 [80000009]\n",
      "76:  0.0 [80000009]\n",
      "77:  0.0 [80000009]\n",
      "78:  0.0 [80000009]\n",
      "79:  0.0 [80000009]\n",
      "80:  0.0 [80000009]\n",
      "81:  0.0 [80000009]\n",
      "82:  0.0 [80000009]\n",
      "83:  0.0 [80000009]\n",
      "84:  0.0 [80000009]\n",
      "85:  0.0 [80000009]\n",
      "86:  0.0 [80000009]\n",
      "87:  0.0 [80000009]\n",
      "88:  0.0 [80000009]\n",
      "89:  0.0 [80000009]\n",
      "90:  0.0 [80000009]\n",
      "91:  0.0 [80000009]\n",
      "92:  0.0 [80000009]\n",
      "93:  0.0 [80000009]\n",
      "94:  0.0 [80000009]\n",
      "95:  0.0 [80000009]\n",
      "96:  0.0 [80000009]\n",
      "97:  0.0 [80000009]\n",
      "98:  0.0 [80000009]\n",
      "99:  0.0 [80000009]\n",
      "100:  0.0 [80000009]\n",
      "101:  0.0 [80000009]\n",
      "102:  0.0 [80000009]\n",
      "103:  0.0 [80000009]\n",
      "104:  0.0 [80000009]\n",
      "105:  0.0 [80000009]\n",
      "106:  0.0 [80000009]\n",
      "107:  0.0 [80000009]\n",
      "108:  0.0 [80000009]\n",
      "109:  0.0 [80000009]\n",
      "110:  0.0 [80000009]\n",
      "111:  0.0 [80000009]\n",
      "112:  0.0 [80000009]\n",
      "113:  0.0 [80000009]\n",
      "114:  0.0 [80000009]\n",
      "115:  0.0 [80000009]\n",
      "116:  0.0 [80000009]\n",
      "117:  0.0 [80000009]\n",
      "118:  0.0 [80000009]\n",
      "119:  0.0 [80000009]\n",
      "120:  0.0 [80000009]\n",
      "121:  0.0 [80000009]\n",
      "122:  0.0 [80000009]\n",
      "123:  0.0 [80000009]\n",
      "124:  0.0 [80000009]\n",
      "125:  0.0 [80000009]\n",
      "126:  0.0 [80000009]\n",
      "127:  0.0 [80000009]\n",
      "128:  0.0 [80000009]\n",
      "129:  0.0 [80000009]\n",
      "130:  0.0 [80000009]\n",
      "131:  0.0 [80000009]\n",
      "132:  0.0 [80000009]\n",
      "133:  0.0 [80000009]\n",
      "134:  0.0 [80000009]\n",
      "135:  0.0 [80000009]\n",
      "136:  0.0 [80000009]\n",
      "137:  0.0 [80000009]\n",
      "138:  0.0 [80000009]\n",
      "139:  0.0 [80000009]\n",
      "140:  0.0 [80000009]\n",
      "141:  0.0 [80000009]\n",
      "142:  0.0 [80000009]\n",
      "143:  0.0 [80000009]\n",
      "144:  0.0 [80000009]\n",
      "145:  0.0 [80000009]\n",
      "146:  0.0 [80000009]\n",
      "147:  0.0 [80000009]\n",
      "148:  0.0 [80000009]\n",
      "149:  0.0 [80000009]\n",
      "150:  0.0 [80000009]\n",
      "151:  0.0 [80000009]\n",
      "152:  0.0 [80000009]\n",
      "153:  0.0 [80000009]\n",
      "154:  0.0 [80000009]\n",
      "155:  0.0 [80000009]\n",
      "156:  0.0 [80000009]\n",
      "157:  0.0 [80000009]\n",
      "158:  0.0 [80000009]\n",
      "159:  0.0 [80000009]\n",
      "160:  0.0 [80000009]\n",
      "161:  0.0 [80000009]\n",
      "162:  0.0 [80000009]\n",
      "163:  0.0 [80000009]\n",
      "164:  0.0 [80000009]\n",
      "165:  0.0 [80000009]\n",
      "166:  0.0 [80000009]\n",
      "167:  0.0 [80000009]\n",
      "168:  0.0 [80000009]\n",
      "169:  0.0 [80000009]\n",
      "170:  0.0 [80000009]\n",
      "171:  0.0 [80000009]\n",
      "172:  0.0 [80000009]\n",
      "173:  0.0 [80000009]\n",
      "174:  0.0 [80000009]\n",
      "175:  0.0 [80000009]\n",
      "176:  0.0 [80000009]\n",
      "177:  0.0 [80000009]\n",
      "178:  0.0 [80000009]\n",
      "179:  0.0 [80000009]\n",
      "180:  0.0 [80000009]\n",
      "181:  0.0 [80000009]\n",
      "182:  0.0 [80000009]\n",
      "183:  0.0 [80000009]\n",
      "184:  0.0 [80000009]\n",
      "185:  0.0 [80000009]\n",
      "186:  0.0 [80000009]\n",
      "187:  0.0 [80000009]\n",
      "188:  0.0 [80000009]\n",
      "189:  0.0 [80000009]\n",
      "190:  0.0 [80000009]\n",
      "191:  0.0 [80000009]\n",
      "192:  0.0 [80000009]\n",
      "193:  0.0 [80000009]\n",
      "194:  0.0 [80000009]\n",
      "195:  0.0 [80000009]\n",
      "196:  0.0 [80000009]\n",
      "197:  0.0 [80000009]\n",
      "198:  0.0 [80000009]\n",
      "199:  0.0 [80000009]\n",
      "200:  0.0 [80000009]\n",
      "201:  0.0 [80000009]\n",
      "202:  0.0 [80000009]\n",
      "203:  0.0 [80000009]\n",
      "204:  0.0 [80000009]\n",
      "205:  0.0 [80000009]\n",
      "206:  0.0 [80000009]\n",
      "207:  0.0 [80000009]\n",
      "208:  0.0 [80000009]\n",
      "209:  0.0 [80000009]\n",
      "210:  0.0 [80000009]\n",
      "211:  0.0 [80000009]\n",
      "212:  0.0 [80000009]\n",
      "213:  0.0 [80000009]\n",
      "214:  0.0 [80000009]\n",
      "215:  0.0 [80000009]\n",
      "216:  0.0 [80000009]\n",
      "217:  0.0 [80000009]\n",
      "218:  0.0 [80000009]\n",
      "219:  0.0 [80000009]\n",
      "220:  0.0 [80000009]\n",
      "221:  0.0 [80000009]\n",
      "222:  0.0 [80000009]\n",
      "223:  0.0 [80000009]\n",
      "224:  0.0 [80000009]\n",
      "225:  0.0 [80000009]\n",
      "226:  0.0 [80000009]\n",
      "227:  0.0 [80000009]\n",
      "228:  0.0 [80000009]\n",
      "229:  0.0 [80000009]\n",
      "230:  0.0 [80000009]\n",
      "231:  0.0 [80000009]\n",
      "232:  0.0 [80000009]\n",
      "233:  0.0 [80000009]\n",
      "234:  0.0 [80000009]\n",
      "235:  0.0 [80000009]\n",
      "236:  0.0 [80000009]\n",
      "237:  0.0 [80000009]\n",
      "238:  0.0 [80000009]\n",
      "239:  0.0 [80000009]\n",
      "240:  0.0 [80000009]\n",
      "241:  0.0 [80000009]\n",
      "242:  0.0 [80000009]\n",
      "243:  0.0 [80000009]\n",
      "244:  0.0 [80000009]\n",
      "245:  0.0 [80000009]\n",
      "246:  0.0 [80000009]\n",
      "247:  0.0 [80000009]\n",
      "248:  0.0 [80000009]\n",
      "249:  0.0 [80000009]\n",
      "250:  0.0 [80000009]\n",
      "251:  0.0 [80000009]\n",
      "252:  0.0 [80000009]\n",
      "253:  0.0 [80000009]\n",
      "254:  0.0 [80000009]\n",
      "255:  0.0 [80000009]\n"
     ]
    }
   ],
   "source": [
    "# check that the model we generated is good.\n",
    "for i in range(0, 256):\n",
    "    bias, error_states = InputChecker.run_checker(f\"../all_bad_small_sample/\", i)\n",
    "    print(f\"{i}: \",bias, error_states)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "from dwave.system import DWaveSampler, EmbeddingComposite\n",
    "from greedy import SteepestDescentComposite\n",
    "\n",
    "qpu = EmbeddingComposite(DWaveSampler(solver={\"name\": \"Advantage_system4.1\"}))\n",
    "sampler = SteepestDescentComposite(qpu)\n",
    "result = sampler.sample(bqm, num_reads=7000, chain_strength=1.5)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "0.0"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "result.first.energy"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [],
   "source": [
    "with open(f\"../all_bad_small_sample/context.json\") as json_file:\n",
    "    context = json.load(json_file)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "11110101\n"
     ]
    }
   ],
   "source": [
    "input_qubit_names = context['input']\n",
    "res = \"\"\n",
    "for name in input_qubit_names:\n",
    "    res += str(result.first.sample[name])\n",
    "print(res[::-1])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "11110101\n",
      "11010111\n",
      "11010100\n",
      "11000100\n",
      "11110110\n",
      "11100000\n",
      "10100010\n",
      "11000000\n",
      "11110000\n"
     ]
    }
   ],
   "source": [
    "for low in result.lowest():\n",
    "    res = \"\"\n",
    "    for name in input_qubit_names:\n",
    "        res += str(low[name])\n",
    "    print(res[::-1])"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 64 bit small sample"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "````bash\n",
    "./modeler -c u3.c - 0 --no-syscall-id-check --no-exit-code-check --no-division-by-zero-check --no-address-alignment-check --constant-propagation --linear-address-space\n",
    "````"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "started building ../btor2files/u3-64.btor2 for 15 timesteps\n",
      "{'size_datasegment': 2, 'size_heap': 1, 'size_stack': 9, 'begin_datasegment': 8704, 'begin_heap': 9216, 'word_size': 64, 'address_step_size': 1, 'address_word_size': 29, 'begin_stack': 536870912}\n",
      "output dir:  ../64bit_small_sample/\n",
      "sort memory modified to be bitvector of size:  768\n"
     ]
    }
   ],
   "source": [
    "parser = BTor2BQM(15)\n",
    "bqm = parser.parse_file(f\"../btor2files/u3-64.btor2\",\n",
    "                  f\"../64bit_small_sample/\",\n",
    "                  with_init=True, modify_memory_sort=True)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "404"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "len(bqm.linear.keys())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 26,
   "metadata": {},
   "outputs": [],
   "source": [
    "from dwave.system import DWaveSampler, EmbeddingComposite\n",
    "from greedy import SteepestDescentComposite\n",
    "\n",
    "qpu = EmbeddingComposite(DWaveSampler(solver={\"name\": \"Advantage_system4.1\"}))\n",
    "sampler = SteepestDescentComposite(qpu)\n",
    "result = sampler.sample(bqm, num_reads=5000, chain_strength=1.5)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 27,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "0.0"
      ]
     },
     "execution_count": 27,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "result.first.energy"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "00111011\n"
     ]
    }
   ],
   "source": [
    "with open(f\"../64bit_small_sample/context.json\") as json_file:\n",
    "    context = json.load(json_file)\n",
    "input_qubit_names = context['input']\n",
    "for low in result.lowest():\n",
    "    res = \"\"\n",
    "    for name in input_qubit_names:\n",
    "        res += str(low[name])\n",
    "    print(res[::-1])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "0.0"
      ]
     },
     "execution_count": 30,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Without steepest gradient descent\n",
    "from dwave.system import DWaveSampler, EmbeddingComposite\n",
    "from greedy import SteepestDescentComposite\n",
    "\n",
    "qpu = EmbeddingComposite(DWaveSampler(solver={\"name\": \"Advantage_system4.1\"}))\n",
    "# sampler = SteepestDescentComposite(qpu)\n",
    "result = qpu.sample(bqm, num_reads=7000, chain_strength=1.5)\n",
    "result.first.energy"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "01010011\n"
     ]
    }
   ],
   "source": [
    "with open(f\"../64bit_small_sample/context.json\") as json_file:\n",
    "    context = json.load(json_file)\n",
    "input_qubit_names = context['input']\n",
    "for low in result.lowest():\n",
    "    res = \"\"\n",
    "    for name in input_qubit_names:\n",
    "        res += str(low[name])\n",
    "    print(res[::-1])"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.6"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 1
}
